NO 1.393 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be disproven:



↳ HASKELL
  ↳ BR

mainModule Main
  ((repeat :: a  ->  [a]) :: a  ->  [a])

module Main where
  import qualified Prelude


Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR

mainModule Main
  ((repeat :: a  ->  [a]) :: a  ->  [a])

module Main where
  import qualified Prelude


Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed

mainModule Main
  ((repeat :: a  ->  [a]) :: a  ->  [a])

module Main where
  import qualified Prelude


Let/Where Reductions:
The bindings of the following Let/Where expression
xs
where 
xs  = x : xs

are unpacked to the following functions on top level
repeatXs vx = vx : repeatXs vx



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
              ↳ Narrow

mainModule Main
  (repeat :: a  ->  [a])

module Main where
  import qualified Prelude


Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
                ↳ QDP
                  ↳ NonTerminationProof
              ↳ Narrow

Q DP problem:
The TRS P consists of the following rules:

new_repeatXs(vy3, ba) → new_repeatXs(vy3, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_repeatXs(vy3, ba) → new_repeatXs(vy3, ba)

The TRS R consists of the following rules:none


s = new_repeatXs(vy3, ba) evaluates to t =new_repeatXs(vy3, ba)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_repeatXs(vy3, ba) to new_repeatXs(vy3, ba).




Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ LetRed
            ↳ HASKELL
              ↳ Narrow
              ↳ Narrow
                ↳ QDP
                  ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

new_repeatXs(vy3, ba, []) → new_repeatXs(vy3, ba, [])

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

new_repeatXs(vy3, ba, []) → new_repeatXs(vy3, ba, [])

The TRS R consists of the following rules:none


s = new_repeatXs(vy3, ba, []) evaluates to t =new_repeatXs(vy3, ba, [])

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from new_repeatXs(vy3, ba, []) to new_repeatXs(vy3, ba, []).